% \newcommand{\simIOo}{\mathrel{\sim_{\tt IO}^{\tt o}}} % 
\newcommand{\simHO}{\mathrel{\sim_{\tt HO}}} % 
\newcommand{\simHOo}{\mathrel{\sim^{\tt o}_{\tt HO}}} % 
\newcommand{\simNORo}{\mathrel{\sim_{\tt NOR}^{\tt o}}} % 
\newcommand{\simNORex}{\mathrel{\sim_{\tt NOR}^\star}} % 
\newcommand{\simNOR}{\mathrel{\sim_{\tt NOR}}} % 
\newcommand{\simCON}{\mathrel{\sim_{\tt CON}}} % 
\newcommand{\simNORasy}{\mathrel{\sim_{\tt NOR}^{\tt asy}}} %
%\newcommand{\PrOp}{\mbox{AHO$\pi$}}  %processes
\newcommand{\PrOp}{\mbox{\ahopi}}  %processes
\newcommand{\PrClo}{\PrOp^\bullet}  %closed processes


\def\reff#1{(\ref{#1})}       %references between brackets




% general  utility

\def\finish#1{}
%\def\finish#1 {\vskip.2cm\noindent{\em #1}%
%   \marginpar{$\longleftarrow$}\vskip.2cm}
%{}



\renewcommand{\tilde}{\widetilde}
\newcommand{\dom}[1]{{\ccc{dom}}(#1)} % the domain of something  


      
   % for  frames

\newcommand{\myframe}[2]{\bigskip\noindent {\large\bf #1}\noindent \[\framebox{#2}\]}

\newcommand{\myframearray}[1]{$\begin{array}{cr}
\myspaceframe{2}
 #1 \end{array}$}

 \newcommand{\mytextw}{\textwidth} 

      

% names and variables

\def\Names{{\cal N}}
\def\fn#1{\ccc{fn}(#1)}         % free names
\def\bn#1{\ccc{bn}(#1)}         % bound names
\def\en#1{\ccc{en}(#1)}         % extruded names
\def\n#1{\ccc{n}(#1)}           % names

\def\fv#1{\ccc{fv}(#1)}         % free variables
\def\bv#1{\ccc{bv}(#1)}         % bound variables

% processes

%\newcommand{\obj}[1]{\langle #1 \rangle}
\def\nil{{\boldsymbol 0}}
\def\res#1{{\boldsymbol \nu} #1\:}   % restriction
\def\resb#1{({\boldsymbol \nu} #1)\:}   % restriction  with brackets
\def\rest#1#2{({\boldsymbol \nu} #1 : #2)\:} % typed restriction



\mathcode`\!="4021 % `!' as prefix operator
\mathcode`\.="602E

%\mathcode`\!="4021 % `!' as prefix operator
\mathcode`\|="326A % `|' as relation operator
%\mathcode`\.="602E

\def\mat#1#2{[#1 \mathop{=} #2]}           % matching
\def\mismat#1#2{[#1 \mathop{\neq} #2]}     % mismatching

\def\sub#1#2{\{\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}\}}
\def\suba#1#2{\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}}
\def\subSMALL#1#2{{\small\{\raisebox{.5ex}{\scriptsize$#1$}\! /
    \!\mbox{\scriptsize$#2$}\}}}  % substitutions, smaller characters
                                  % (useful in labeled transitions)





\newcommand{\outO}[2]{\overline{#1}\obj{#2}}     
\newcommand{\out}[2]{\overline{#1}{#2}}     
\def\inp#1#2{#1(#2)}


\newcommand{\outF}[2]{\overline{#1}{#2}} % output without angle
                                              % brackets and no space

\newcommand{\outFS}[2]{\overline{#1}\,{#2}} % output without angle
                                              % brackets and little
                                              % space before the
                                              % object


\newcommand{\outSS}[2]{\overline{#1}\,{#2}\, }% as before, but also
                                              % space after object


%\newcommand{\outC}[1]{\overline{#1}}      % CCS  output
\newcommand{\inpC}[1]{#1}                 % CCS  input


% special term construct 
\newcommand{\wrong}{\myccc{wrong}}       % wrong process in typed calculi


\newcommand{\cond}[3]{\begin{array}[t]{@{}l}\myccc{if}\ #1\
  \\ \myccc{then}\ #2\ \\ \myccc{else}\ #3\end{array}}

\newcommand{\myif}{\myspace{\myccc{if}}\myspace}               % if-then-else
\newcommand{\mythen}{\myspace{\myccc{then}}\myspace}               % if-then-else
\newcommand{\myelse}{\myspace{\myccc{else}}\myspace}               % if-then-else



\newcommand{\lett}{\myccc{let}}
\newcommand{\letin}[2]{\; \: \lett\ {#1}\;\:  \myccc{in}\ #2}
\newcommand{\letinAR}[2]{\begin{array}[t]{@{}l}\lett\ #1\
 \\ \myccc{in}\ #2\end{array}}

 
% special prefixes

\def\outUNDER#1#2{\underline{\overline{#1}\obj{#2}}}
                  % output underlined 
\def\inpUNDER#1#2{\underline{#1(#2)}}
                  % input underlined  

   


% reductions
\newcommand{\ra}{\longrightarrow}        
\newcommand{\Ra}{\Longrightarrow} 




\newcommand{\rad}{\arr\tau_{\myrm{d}}} % deterministic reduction


%convergence

\newcommand{\Dwa}{\Downarrow}           % plain convergence
\newcommand{\dwa}{\downarrow}           % plain convergence


 
% transizioni

%\def\arrep#1{\:\stackrel{#1}{\mbox{\rightarrowfill}_{!}}\:}
\newcommand{\arr}[1]{\mathrel{\stackrel{{\;\;#1\;\;}}{\mbox{\rightarrowfill}}}}
                                %  strong arrow 
%{\mathrel{"-{^{#1}}!>"}}


\def \rightarrowfillWEAK{$\m@th\mathord{\smash=}\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord{\smash=}\mkern-2mu$}\hfill
  \mkern-6mu\mathord\Rightarrow$}


\newcommand{\Ar}[1]{\mathrel{\stackrel{{\;\;#1\;\;}}{\mbox{\rightarrowfillWEAK}}}} 
                                    %weak  labelled transitions


%\newcommand{\Ar}[1]{\mathrel{\stackrel{{\;\;#1\;\;}}{\Longrightarrow}}} 
                                    %weak  labelled transitions
%{\mathrel{"={^{#1}}!>"}}
                                    
\newcommand{\arcap}[1]{\mathrel{\stackrel{{\;\; {\widehat{#1}} \;\;}}{\mbox{\rightarrowfill}}}} 
%{\mathrel{"-{^{\widehat{#1}}}!>"}}
 %{\:\stackrel{{\widehat{#1}}}{\ra}\:}
                                    %strong labelled transitions with hat
\newcommand{\Arcap}[1]{\mathrel{\stackrel{{\;\;{\widehat{#1}}\;\;}}{\mbox{\rightarrowfillWEAK}}}}
%{\mathrel{"={^{\widehat{#1}}}!>"}}
%{\:\stackrel{{\widehat{#1}}}{\Longrightarrow}\:}
                                    %weak labelled transitions with   hat
                                    

% actions

\newcommand{\sbj}[1]{\ccc{subj}(#1)} % subject of an action

                                    

\def\iae#1#2{{#1}{#2}} % input action in the early style
\def\ia#1#2{{#1}{(#2)}} % input action in the late style



\newcommand{\inpbound}[2]{#1(#2)}  % input bound 

\newcommand{\oa}[3]{(\res{#1})\out{#2}{#3}} % output action, with
                                            % restriction 
%\newcommand{\oaF}[3]{(\res{#1})\outFS{#2}{#3}}% output action, with
%                                            % restriction, no bracket
%\newcommand{\oaNS}[3]{(\res{#1})\outF{#2}{#3}}% output action, with
%                                            % restriction, no bracket
%                                            % and no space



\newcommand{\boat}[4]{\rest{#1}{#2}\outA {#3}{#4}} %bound output action typed
\newcommand{\boa}[3]{\resb{#1}{\outA {#2}{#3}}} %bound output action untyped

% without angle brackets::
\newcommand{\boaFt}[4]{\rest{#1}{#2}\outFS {#3}{#4}} %bound output action typed
\newcommand{\boaNSt}[4]{\rest{#1}{#2}\outF {#3}{#4}} %bound output
                                                     %action typed, no 
                                                     %space

\newcommand{\boaF}[3]{\resb{#1}{\outFS {#2}{#3}}} %bound output action
                                                 %untyped
\newcommand{\boaNS}[3]{\resb{#1}{\outF {#2}{#3}}} %bound output action
                                                  %untyped, no space




\def\iaeF#1#2{{#1}\,{#2}} % input action in the early style without brackets
\def\iaeNS#1#2{{#1}{#2}} % input action in the early style without
                          % brackets and without space



%% for open processes 
\newcommand{\gt}[1]{ G {#1} }
\newcommand{\qgt}{ G  }      
\newcommand{\gtH}[1]{ H {#1} }
\newcommand{\qgtH}{ H  }      

\newcommand{\gtHp}[1]{ H' {#1} }  
\newcommand{\qgtHp}{ H'  }          

\newcommand{\gtHpp}[1]{ H'' {#1} }
\newcommand{\qgtHpp}{ H''  }       


\newcommand{\gtp}[1]{ G' {#1} }         
\newcommand{\qgtp}{ G'  }

\newcommand{\gtpp}[1]{ G'' {#1} }  %primed context       
\newcommand{\qgtpp}{ G''  }



% FOR CONTEXTS

\newcommand{\brac}[1]{[#1] }   % brackets for the context hole

\newcommand{\contexthole}{ [ \cdot  ] }      %hole of a context
\newcommand{\holE}{\contexthole}  % hole


\newcommand{\ct}[1]{ C \brac{#1} }   %filled context
\newcommand{\qct}{ C  }              %unfilled context  
\newcommand{\holei}[1]{[\cdot]_{#1}}  %i-th hole

\newcommand{\ctD}[1]{ D \brac{#1} }   %filled context
\newcommand{\qctD}{ D  }              %unfilled context  

\newcommand{\ctDp}[1]{ D' \brac{#1} }   %filled context
\newcommand{\qctDp}{ D'  }              %unfilled context  

\newcommand{\ctDpp}[1]{ D'' \brac{#1} }   %filled context
\newcommand{\qctDpp}{ D''  }              %unfilled context  


\newcommand{\ctp}[1]{ C' \brac{#1} }  %primed context       
\newcommand{\qctp}{ C'  }

\newcommand{\ctpp}[1]{ C'' \brac{#1} }  %primed context       
\newcommand{\qctpp}{ C''  }

\newcommand{\ctii}[3]{C_{#1}^{#2} \brac{#3}}

\newcommand{\cti}[2]{C_{#1} \brac{#2}}  %indexed context       
\newcommand{\qcti}[1]{C_{#1}}

\newcommand{\ctip}[2]{C'_{#1} \brac{#2}}  %indexed context       
\newcommand{\qctip}[1]{C'_{#1}}


%% style commands
\newcommand{\ccc}{\mytextsf} % {\rm\tt{#1}}}  %{\mbox{{\tt #1}}}
\newcommand{\myccc}[1]{{\rm\tt{#1}}} % for keywords like
                                  % ``if'', ``then''  

\newcommand{\myrm}[1]{{\rm{#1}}} % for indices
\newcommand{\mynfSTY}[1]{{\rm{#1}}} % for *-nf in $\lambda$-calculus

\newcommand{\kw}[1]{\mbox{\it #1}}
\newcommand{\kwsmall}[1]{\mbox{{\footnotesize\it #1}}}
\newcommand{\mytextsf}[1]{{{\rm\sf{#1}}}}
\newcommand{\amb}[1]{\mbox{#1}}


%BEHAVIOURAL  EQUIVALENCES and relations
  % alpha conversion 
  \newcommand{\equival}{=} %\mathrel{\equiv_\alpha} 

   %strong cases


\newcommand{\bb}{\;\:\mbox{$\sim \! \!  \! \!\!  \! \!\! \!   
 \raisebox{1.2ex}[0ex][0ex]{  \bfcdot}$}\;\:} %barbed
                                                     %bisimulation
                                                     %withc ontext.



\newcommand{\bfcdotB}{ {\mbox{\boldmath $.$}}  }         

\newcommand{\strongbarbedbis}
{\mathrel{\stackrel{\bfcdotB}{\sim}}}
%OLD
%{\mbox{ $\sim  \! \!\! \! \! \! \! \! \!          
% \raisebox{1.2ex}[0ex][0ex]{  \bfcdot} \; \,$}}


% \newcommand{\sbb}{\mathrel{\strongbarbedbis}}
 \newcommand{\sbc}{\simeq}

% %\newcommand{\sbes}{\simeq^{\myrm s}}
%    % barbed equivalence with substitutions 
% \newcommand{\wbes}{\cong^{\myrm s}}
%    % barbed equivalence with substitutions 

% weak cases
  % barbed
\newcommand{\bfcdot}{ {\mbox{\boldmath $ \cdot$}}  }         

\newcommand{\barbedbis}
{\mathrel{\stackrel{\bfcdotB}{\ctxteq}}}

%OLD:
%{\mbox{ $\approx \! \! \! \!\! \!\!        
%\raisebox{1.15ex}[0ex][0ex]{\bfcdot} \; \,$}}

\newcommand{\wbb}{\mathrel{\barbedbis}}
\newcommand{\wbbd}[1]{\mathrel{\barbedbis_{#1}}}
\newcommand{\wbe}{\cong}
\newcommand{\wbc}{\cong^{\myrm c}}
\newcommand{\wbct}[1]{\cong^{\myrm c}_{#1}} % typed bc


\newcommand{\web}{\mathrel{\approx}}
\newcommand{\webRB}{\mathrel{\cong}}

%% probably try to eliminate the 2 macros below (used in HOPi chapter)
%%\newcommand{\webAw}{\mathrel{\approx_{\myccc{a},w}}}%weak bisimulation in piAw
%%\newcommand{\wbcSPEC}[3]{#1 \vdash #2 \wbc #3}
%%      % #2 and #3 are weak barbed congruence in the calculus #1



  % early bisimulation and congruence
\newcommand{\wec}{\mathrel{\approx^{\myrm c}}}


% expansion (defined in a similar way to early bisimulation)
\newcommand{\contr}{\mathrel{\succeq}} %\gtrsim
\newcommand{\expa}{\mathrel{\preceq}} %\lesssim
\newcommand{\zcontr}{\mathrel{\succeq}} %\gtrsim
\newcommand{\zexpa}{\mathrel{\preceq}} %\lesssim

% expansion congruence (preserved by substitutions, like early
% congruence)

\newcommand{\contrc}{\mathrel{^{\myrm c}\!\!\succeq}}  % \gtrsim
\newcommand{\expac}{\mathrel{\preceq^{\myrm c}}} %\lesssim


\newcommand{\contrG}{\mathrel{_{\myrm g}\!\!\succeq}}  % ground version
\newcommand{\expaG}{\mathrel{\preceq_{\myrm g}}} % ground version


% early bisimulation and congruence
% \newcommand{\seb}{\mathrel{\sim}} % strong early bisimulation
% \newcommand{\secc}{\seb}  % {\mathrel{\sim^{\myrm c}}} % strong early congruence


% \newcommand{\sgb}{\mathrel{\sim_{\myrm g}}} % strong ground bisimulation
% \newcommand{\wgb}{\mathrel{\approx_{\myrm g}}} % weak ground bisimulation




% TYPED BEHAVIOURAL EQUIVALENCES (there is a mess in these macros)

 

%  special relations

%\def\R{{\cal R}}
\def\RR{\mathrel{\cal R}}
\def\S{{\cal S}}
\def\SS{\mathrel{\cal S}}

 \def\E{{\cal E}}
\def\EE{\mathrel{\cal E}}
 \def\F{{\cal F}}
\def\FF{\mathrel{\cal F}}

%\def\V{{\cal E}}
%\def\VV{\mathrel{\cal E}}
\def\W{{\cal F}}
\def\WW{\mathrel{\cal F}}

\def\X{{\cal X}}
\def\XX{\mathrel{\cal X}}

\def\Y{{\cal Y}}
\def\YY{\mathrel{\cal Y}}
\newcommand{\Xv}[1]{\mathrel{{\X_{#1}}}}
\newcommand{\Yv}[1]{\mathrel{{\Y_{#1}}}}
\newcommand{\Xrv}[1]{\mathrel{{\X^{\rightarrow\star }_{#1}}}}
\newcommand{\Yrv}[1]{\mathrel{{\Y^{\rightarrow\star }_{#1}}}}

\newcommand{\Xfv}[1]{\mathrel{{\X^{\star }_{#1}}}}
\newcommand{\Yfv}[1]{\mathrel{{\Y^{\star }_{#1}}}}

\newcommand{\XCc}[2]{\, \mathrel{{\X^{{\rm c}}_{#1\sepa #2}}}\,}
\newcommand{\YCc}[2]{\,\mathrel{{\Y^{{\rm c}}_{#1\sepa #2}}}\,}
\newcommand{\XCCc}[2]{\, \mathrel{{\X^{{\rm c1}}_{#1\sepa #2}}}\,}


\newcommand{\Xc}[2]{\, \mathrel{{\X_{#1\sepa #2}}}\,}
\newcommand{\Yc}[2]{\,\mathrel{{\Y_{#1\sepa #2}}}\,}
\newcommand{\simc}[2]{\,\mathrel{{\approx_{#1\sepa #2}}}\,}
\newcommand{\simEBc}[2]{\,\mathrel{{\approx_{#1\sepa #2}}}\,}


\newcommand{\simSTRONG}{\mathrel{{\sim}}} % the strong bisimilarity


\newcommand{\simv}[1]{\mathrel{{\approx_{#1}}}}
\newcommand{\simvo}[1]{\mathrel{{\approx^o_{#1}}}}
\newcommand{\simVV}[1]{\mathrel{{\widehat{\approx}_{#1}}}}
\newcommand{\simVVo}[1]{\mathrel{{\widehat{\approx}^o_{#1}}}}

\newcommand{\simEBv}[1]{\mathrel{{\approx_{#1}}}}
\newcommand{\simEBvo}[1]{\mathrel{{\approx^o_{#1}}}}
\newcommand{\simEBVV}[1]{\mathrel{{\widehat{\approx}_{#1}}}}
\newcommand{\simEBVVo}[1]{\mathrel{{\widehat{\approx}^o_{#1}}}}

\newcommand{\simEB}{\approx}
\newcommand{\simEBeq}{\simeq}


\newcommand{\tauLAW}{\succ_\tau} % equality given by tau.R =R






%SPECIAL SYMBOLS

\newcommand{\Mybar}%{\hrulefill} % separation symbol in
                                           % grammars               
{\noindent \rule{\hsize}{0.5mm}} % bar in tables



\newcommand{\MybarUP}{\hrulefill\gp} % separation symbol top table


\def\midd{\; \; \mbox{\Large{$\mid$}}\;\;}




\def\st{\; {\rm{s.t.} \;}}

   % defuguale
\def\defi{\stackrel{\mbox{\scriptsize def}}{=}}

\newcommand{\til}[1]{\widetilde{#1}}
\newcommand{\tilX}{{\til x}}

\newcommand{\bottom}{\perp}

   % qed symbol; causes problems...

%\def\qed{\unskip\nobreak\hfil\penalty50\hskip1em\null\nobreak\hfil
%  $\Box$\parfillskip=0pt\finalhyphendemerits=0\endgraf}
                                        % square end environments
%\newcommand{\NEWqed}{{\qed}} % for end of theorems, def, etc, that do
                           % not have a proof afterwards



%% for inference rules



\newcommand{\infrule}[3]{\[
{\trans{#1}\quadrule \displaystyle{#2 \over #3} } %\\[10pt]
\]}
\newcommand{\infruleSIDE}[4]{\[
{\trans{#1}\quadrule\displaystyle{#2 \over #3}\;\; #4 } %\\[10pt]
\]}  % inf rule with a side condition
\newcommand{\shortinfrule}[3]{ {\trans{#1}}: \quadrule
     \displaystyle{#2 \over #3}}
\newcommand{\shortinfruleSIDE}[4]{ {\trans{#1}} \quadrule
     \displaystyle{#2 \over #3}\;\; #4}

\newcommand{\shortaxiom}[2]{{\trans{#1}}\quadrule
\displaystyle{ \over #2}}


\newcommand{\shortaxiomE}[2]{{\trans{#1}}:\quadrule
\displaystyle{ #2}}

\newcommand{\myinf}[3]{{\rn{#1}}\quadrule \displaystyle{#2 \over #3} }
    % for  plain  inference rules

\def\trans#1{\rn{#1}}   % for the names of transition rules
\newcommand{\rn}[1]{%
  \ifmmode 
    \mathchoice
      {\mbox{\sc #1}}
      {\mbox{\sc #1}}
      {\mbox{\small\sc #1}}
      {\mbox{\tiny\uppercase{#1}}}%
  \else
    {\sc #1}%
  \fi}

\newcommand{\quadrule}{\hskip .2cm }

\newcommand{\andalso}{\quad\quad}


% various ``for each''
\newcommand{\Fforeachi}[2]{\mbox{for each $\myin i {#1}{#2}$}\ \ }
\newcommand{\Fforeachj}[2]{\mbox{for each $\myin j {#1}{#2}$}\ \ }
\newcommand{\Fforeachij}[4]{\mbox{for each $\myin i {#1}{#2}$ and
$\myin j {#3}{#4}$}\ \ } 

\newcommand{\foreachi}{\mbox{for each $i$,}\ \ }
\newcommand{\foreachj}{\mbox{for each $j$,}\ \ }
\newcommand{\foreachij}{\mbox{for each $i$ and $j$,}\ \ }









% distance points
\newcommand{\Stkp}{2pt} 
\newcommand{\tkp}{6pt} 
\newcommand{\bigtkp}{10pt} 
\newcommand{\Bigtkp}{15pt}
\newcommand{\verybigtkp}{13pt}
\newcommand{\mysp}{13pt}

\newcommand{\hb}{\hskip .5cm }
\newcommand{\hk}{\hskip .5cm }

\newcommand{\mypt}{2pt} 
\newcommand{\mydots}{ ,\ldots, }
\newcommand{\myspace}{\; \,}
\newcommand{\SPACEYSYM}[1]{\mathrel{#1}}


